#ifndef _PDT_CHECKSPEC_H_
#define _PDT_CHECKSPEC_H_

#include "PDTEvalTraversal.h"
#include "PDTFunction.h"
#include "PDTBehavior.h"

#include <string>
#include <map>

using namespace std;

class PDTVar;

class PDTCheckSpec : public PDTEvalTraversal {
    PDTFunctionDec *func;
    PDTBehaviors *behaviors;
    PDTPreCondition *pre;
    PDTPostCondition *post;


    public:
    PDTCheckSpec(PDTCodeGraph & aCG,
            PDTFunctionDec *func,
            PDTBehaviors *behaviors=NULL,
            PDTPreCondition *pre=NULL,
            PDTPostCondition *post=NULL);

    PDTCheckSpec(PDTCodeGraph & aCG, 
            const string & funcName, 
            const string & specName);

    void setFunctionSpecTriple( PDTFunctionDec *func, PDTBehaviors *behaviors=NULL,  PDTPreCondition *pre=NULL,  PDTPostCondition *post=NULL) {
        this->func = func;
        this->behaviors = behaviors;
        this->pre = pre;
        this->post = post;
        clearVariableValues();
    }
    const string & getFuncName() const {
        return func->getName();
    }
    const string & getSpecName() const {
        return behaviors->getName();
    }

    bool buildRanges() ;

    Traversal::RetType applyInput(PDTBehavior * beh) ;
    Traversal::RetType applyOutput(PDTBehavior * beh) ;
    Traversal::RetType execCodeBetweenPreAndPost(
        PDTListOfStatements & list, unsigned int idx);
    bool locateCodeBetweenPreAndPost(
        PDTListOfStatements * & list, unsigned int & idx);

    bool clearVariableValues();

    typedef map<PDTVar *, PDTConst * > VarToValMap;
    bool getOutVariableValues(PDTBehavior * beh, VarToValMap & outValues);
    bool isEqual(VarToValMap& lhs, VarToValMap& rhs);


    bool checkPrePostPrint(PDTBehavior * beh) ;
    bool checkPreCodePostPrint(PDTBehavior * beh, PDTListOfStatements & list, unsigned int idx);

    bool checkPrePost() ;
    bool checkPreCodePost(PDTListOfStatements &list, unsigned int idx);
    void check();

    struct Result {
        PDTBehavior * beh; 
        unsigned int withCode :1;
        unsigned int PofI : 1; 
        unsigned int QofO : 1;
        unsigned int QofOPrime : 1;
        unsigned int oEqOPrime : 1;
        mutable unsigned int success : 1;
        unsigned int unused : 26;

        Result(PDTBehavior * abeh=NULL, bool awithCode=false,
                bool aPofI=false, bool aQofO=false,
                bool aQofOPrime=false, bool aoEqOPrime=false) :
            beh(abeh),
            withCode(awithCode? 1:0),
            PofI(aPofI? 1:0),QofO(aQofO? 1:0),
            QofOPrime(aQofOPrime?1:0), oEqOPrime(aoEqOPrime? 1:0),
            success(1), unused (0)
        {
        }

        const Result & succeeded () const {
            success = 1;
            return *this;
        }
        const Result & failed () const {
            success = 0;
            return *this;
        }
        bool pass()  const {
            if (withCode) {
                if (beh->isGood())
            //ss << "Required: o in g(i) and Q(i,o)" <<endl;
                    return oEqOPrime && QofO ;
                else 
                    return false; // TODO: to be determined
            } else {
                if (beh->isGood())
                    return (!PofI) || QofO;
                else 
                    return PofI && (!QofO);
            }
            return false;
        }
        string advice();
    };

    Result checkPrePost(PDTBehavior * beh) ;
    Result checkPreCodePost(PDTBehavior * beh, PDTListOfStatements & list, unsigned int idx);

    string recommendationString(
            const Result & result ) {
        return recommendationString( result.beh, result.withCode, 
                result.PofI, result.QofO, 
                result.QofOPrime, result.oEqOPrime);
    }

    string recommendationString(
        PDTBehavior * beh, bool withCode,
        bool PofI, bool QofO,
        bool QofOPrime=false, bool oEqOPrime=false) ;

    string advice(
        PDTBehavior * beh, bool withCode,
        bool PofI, bool QofO,
        bool QofOPrime=false, bool oEqOPrime=false) ;
};
#endif
